Чистейше возможный язык

Хочется протестировать, смогу ли я кратко описать в одном абзаце то, что я хочу
получить. Все началось с того, что я хотел сделать для Erlang язык, который бы
не стыдно было показать на конференции по функциональному программированию. Но
сейчас я понимаю, что я ввязался в битву, которая может стать для меня
последней.

Началось все с рассмотрения Morte, как ядра CoC, вершини PTS лямбда куба.
Обычно современные пруверы которые работают в ITT, кроме чистого лямбда
исчисления имеют следуюшие наборы аксиом (оглашаем весь список):

* чистое лямбда исчисление (экспоненциалы, произведения и терминалы)
* fix, in, out
* case/fold, рекурсоры для индуктивных типов
* индексированные вселенные

Семантикой базовых аксиом лямбда исчисления необходимого для построения
категориальной абстрактной машины по Кюрену является всеми горячо любимая ДЗК,
семантикой аксиом (ко)рекурсии являются (ко)терминальные F-(ко)алгебры,
индуктивные (рекурсивные) типы представляют собой закодированные по черчу
конструкции со списком встроенных фолдов, рекурсоров или других служебных
функций. Семантикой индексированных вселенных являются (инфинити,1)-топосы.
Обычно используют кумулятивные вселенные, так как именно они используются в
книге HoTT. Coq поддерживает комулятивные вселенные, в Lean universe
полиморфизм. Но все эти аксиомы в пруверах и даже компактных ядрах типа
PiSigma, встроены в ядро в отличие от Morte. В Lean напирмер индуктивные типы,
как и стрелки являются элементами Type1 в иерархии Prop : Type1 : Type2 ...

ITT = CoC + Universes + Inductive Types

Что предлагаем мы? Мы предлагаем использовать библиотеку кодированых по черчу
индуктивных конструкций вместо аксиом. Так Morte уже идет с турториалом по
схеме кодирования индуктивных типов по черч-лайк схеме Боема-Берардуччи,
поэтому он позволяет избавиться от fix аксиомы, что автоматически решает
проблему нормализации. Все термы в нашем языке полностью нормализированы.
Следующий шаг — это использование вместо звездочки похожего на индуктивный
#Nat, но оличимого, например #Star, типа везде, где используется звездочка
(Type). Таким образом, мы хотим удалить аксиому вселенных, и, наконец,
последний шаг — это написать библиотеку рекурсоров по зависимомому индуктивному
типу для паттерн мачинг конструкций и других целей на самом себе используя
схему кодирования Берардуччи, только кроме фолдов держать еще список других
комбинаторов для индуктивного типа. В Lean например case_on, rec_on,
inductive_on, в PiSigma case/fold, в Charity record,fold,case,unfold.

Таким образом, используя максимально компактное ядро, хотим избавиться от
вещей, которые в остальных пруверах являются аксиомами и встроены в AST
кернела. Таким образом углубится fusion при бета и эта редукциях исходной
программы и повысится компрессия. Мы говорим о компрессии, потому, что лямбда
термы после подстановок могут быть довольно увесистыми и хорошо поддаваться
компрессии.

ОМ ЛЯМБДА ГАРБХА ХУМ